home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / lisp / eulisp / comp0_89.lha / Feel / Boot / Compiler / boyer.em < prev    next >
Lisp/Scheme  |  1993-04-26  |  14KB  |  609 lines
  1. ;; $aclHeader: boyer.cl,v 1.3 90/10/16 11:59:14 layer Rel $
  2.  
  3. ;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
  4. ;;; Fairly CONS intensive.
  5.  
  6. (defmodule boyer
  7.   ((except (member assoc) 
  8.        standard0)
  9.    plists)
  10.   ()
  11.   
  12.   (defun assoc (a l p)
  13.     (cond ((null l) nil)
  14.       ((p a (car (car l)))
  15.        (car l))
  16.       (t (assoc a (cdr l) p))))
  17.  
  18.   (defun member (a l p)
  19.     (cond ((null l) nil)
  20.       ((p a (car l)))
  21.       (t (member a (cdr l) p))))
  22.  
  23.   (defun add-lemma (term)
  24.     (cond ((and (not (atom term))
  25.         (eq (car term)
  26.             (quote equal))
  27.         (not (atom (cadr term))))
  28.        ((setter get) (caadr term) (quote lemmas)
  29.         (cons term (get (caadr term) (quote lemmas)))))
  30.       (t (error "~%ADD-LEMMA did not like term:  ~a" term))))
  31.  
  32.   (defun add-lemma-lst (lst)
  33.     (cond ((null lst)
  34.        t)
  35.       (t (add-lemma (car lst))
  36.          (add-lemma-lst (cdr lst)))))
  37.  
  38.   (defun apply-subst (alist term)
  39.     (cond ((atom term)
  40.        (let ((tmp (assq term alist)))
  41.          (if tmp (cdr tmp)
  42.            term)))
  43.       (t (cons (car term)
  44.            (apply-subst-lst alist (cdr term))))))
  45.  
  46.   (defun apply-subst-lst (alist lst)
  47.     (cond (lst 
  48.        (cons (apply-subst alist (car lst))
  49.          (apply-subst-lst alist (cdr lst))))
  50.       (t nil)))
  51.  
  52.   (defun falsep (x lst)
  53.     (or (equal x (quote (f)))
  54.     (member x lst equal)))
  55.  
  56.   (defun one-way-unify (term1 term2 **unify-subst**)
  57.     (progn ((setter car) **unify-subst** nil)
  58.        (one-way-unify1 term1 term2 **unify-subst**)))
  59.  
  60.   (defun one-way-unify1 (term1 term2 **unify-subst**)
  61.     ;;(format t "Unify: ~a ~a~%" term1 term2)
  62.     (cond ((atom term2)
  63.        (let ((tmp (assq term2 (car **unify-subst**))))
  64.          (if tmp 
  65.          (equal term1 (cdr tmp))
  66.            (progn ((setter car) **unify-subst** (cons (cons term2 term1)
  67.                               (car **unify-subst**)))
  68.               t))))
  69.       ((atom term1)
  70.        nil)
  71.       ((eq  (car term1)
  72.         (car term2))
  73.        (one-way-unify1-&lst (cdr term1)
  74.                 (cdr term2)
  75.                 **unify-subst**))
  76.       (t nil)))
  77.  
  78.   (defun one-way-unify1-&lst (lst1 lst2 **unify-subst**)
  79.     (cond ((null lst1)
  80.        t)
  81.       ((one-way-unify1 (car lst1)
  82.                (car lst2)
  83.                            **unify-subst**)
  84.        (one-way-unify1-&lst (cdr lst1)
  85.                 (cdr lst2)
  86.                 **unify-subst**))
  87.       (t nil)))
  88.  
  89.   (defun rewrite (term)
  90.     (cond ((atom term)
  91.        term)
  92.       (t (rewrite-with-lemmas (cons (car term)
  93.                     (rewrite-args (cdr term)))
  94.                   (get (car term)
  95.                        (quote lemmas))))))
  96.  
  97.   (defun rewrite-args (lst)
  98.     (cond (lst
  99.        (cons (rewrite (car lst))
  100.          (rewrite-args (cdr lst))))
  101.       (t nil)))
  102.  
  103.   (defun rewrite-with-lemmas (term lst)
  104.     (let ((**unify-subst** (cons nil nil)))
  105.       (cond ((null lst)
  106.          term)
  107.         ((one-way-unify term (cadr (car lst)) **unify-subst**)
  108.          (rewrite (apply-subst (car **unify-subst**) (caddr (car lst)))))
  109.         (t (rewrite-with-lemmas term (cdr lst))))))
  110.  
  111.   (defun boyer-setup ()
  112.     (add-lemma-lst
  113.      (quote ((equal (compile form)
  114.             (reverse (codegen (optimize form)
  115.                       (nil))))
  116.          (equal (eqp x y)
  117.             (equal (fix x)
  118.                (fix y)))
  119.          (equal (greaterp x y)
  120.             (lessp y x))
  121.          (equal (lesseqp x y)
  122.             (not (lessp y x)))
  123.          (equal (greatereqp x y)
  124.             (not (lessp x y)))
  125.          (equal (boolean x)
  126.             (or (equal x (t))
  127.             (equal x (f))))
  128.          (equal (iff x y)
  129.             (and (implies x y)
  130.              (implies y x)))
  131.          (equal (even1 x)
  132.             (if (zerop x)
  133.             (t)
  134.               (odd (- x 1))))
  135.          (equal (countps- l pred)
  136.             (countps-loop l pred (zero)))
  137.          (equal (fact- i)
  138.             (fact-loop i 1))
  139.          (equal (reverse- x)
  140.             (reverse-loop x (nil)))
  141.          (equal (divides x y)
  142.             (zerop (remainder y x)))
  143.          (equal (assume-true var alist)
  144.             (cons (cons var (t))
  145.               alist))
  146.          (equal (assume-false var alist)
  147.             (cons (cons var (f))
  148.               alist))
  149.          (equal (tautology-checker x)
  150.             (tautologyp (normalize x)
  151.                 (nil)))
  152.          (equal (falsify x)
  153.             (falsify1 (normalize x)
  154.                   (nil)))
  155.          (equal (prime x)
  156.             (and (not (zerop x))
  157.              (not (equal x (add1 (zero))))
  158.              (prime1 x (- x 1))))
  159.          (equal (and p q)
  160.             (if p (if q (t)
  161.                 (f))
  162.               (f)))
  163.          (equal (or p q)
  164.             (if p (t)
  165.               (if q (t)
  166.             (f))
  167.               (f)))
  168.          (equal (not p)
  169.             (if p (f)
  170.               (t)))
  171.          (equal (implies p q)
  172.             (if p (if q (t)
  173.                 (f))
  174.               (t)))
  175.          (equal (fix x)
  176.             (if (numberp x)
  177.             x
  178.               (zero)))
  179.          (equal (if (if a b c)
  180.             d e)
  181.             (if a (if b d e)
  182.               (if c d e)))
  183.          (equal (zerop x)
  184.             (or (equal x (zero))
  185.             (not (numberp x))))
  186.          (equal (plus (plus x y)
  187.               z)
  188.             (plus x (plus y z)))
  189.          (equal (equal (plus a b)
  190.                (zero))
  191.             (and (zerop a)
  192.              (zerop b)))
  193.          (equal (difference x x)
  194.             (zero))
  195.          (equal (equal (plus a b)
  196.                (plus a c))
  197.             (equal (fix b)
  198.                (fix c)))
  199.          (equal (equal (zero)
  200.                (difference x y))
  201.             (not (lessp y x)))
  202.          (equal (equal x (difference x y))
  203.             (and (numberp x)
  204.              (or (equal x (zero))
  205.                  (zerop y))))
  206.          (equal (meaning (plus-tree (append x y))
  207.                  a)
  208.             (plus (meaning (plus-tree x)
  209.                    a)
  210.               (meaning (plus-tree y)
  211.                    a)))
  212.          (equal (meaning (plus-tree (plus-fringe x))
  213.                  a)
  214.             (fix (meaning x a)))
  215.          (equal (append (append x y)
  216.                 z)
  217.             (append x (append y z)))
  218.          (equal (reverse (append a b))
  219.             (append (reverse b)
  220.                 (reverse a)))
  221.          (equal (times x (plus y z))
  222.             (plus (times x y)
  223.               (times x z)))
  224.          (equal (times (times x y)
  225.                z)
  226.             (times x (times y z)))
  227.          (equal (equal (times x y)
  228.                (zero))
  229.             (or (zerop x)
  230.             (zerop y)))
  231.          (equal (exec (append x y)
  232.               pds envrn)
  233.             (exec y (exec x pds envrn)
  234.               envrn))
  235.          (equal (mc-flatten x y)
  236.             (append (flatten x)
  237.                 y))
  238.          (equal (member x (append a b))
  239.             (or (member x a)
  240.             (member x b)))
  241.          (equal (member x (reverse y))
  242.             (member x y))
  243.          (equal (length (reverse x))
  244.             (length x))
  245.          (equal (member a (intersect b c))
  246.             (and (member a b)
  247.              (member a c)))
  248.          (equal (nth (zero)
  249.              i)
  250.             (zero))
  251.          (equal (exp i (plus j k))
  252.             (times (exp i j)
  253.                (exp i k)))
  254.          (equal (exp i (times j k))
  255.             (exp (exp i j)
  256.              k))
  257.          (equal (reverse-loop x y)
  258.             (append (reverse x)
  259.                 y))
  260.          (equal (reverse-loop x (nil))
  261.             (reverse x))
  262.          (equal (count-list z (sort-lp x y))
  263.             (plus (count-list z x)
  264.               (count-list z y)))
  265.          (equal (equal (append a b)
  266.                (append a c))
  267.             (equal b c))
  268.          (equal (plus (remainder x y)
  269.               (times y (quotient x y)))
  270.             (fix x))
  271.          (equal (power-eval (big-plus1 l i base)
  272.                 base)
  273.             (plus (power-eval l base)
  274.               i))
  275.          (equal (power-eval (big-plus x y i base)
  276.                 base)
  277.             (plus i (plus (power-eval x base)
  278.                   (power-eval y base))))
  279.          (equal (remainder y 1)
  280.             (zero))
  281.          (equal (lessp (remainder x y)
  282.                y)
  283.             (not (zerop y)))
  284.          (equal (remainder x x)
  285.             (zero))
  286.          (equal (lessp (quotient i j)
  287.                i)
  288.             (and (not (zerop i))
  289.              (or (zerop j)
  290.                  (not (equal j 1)))))
  291.          (equal (lessp (remainder x y)
  292.                x)
  293.             (and (not (zerop y))
  294.              (not (zerop x))
  295.              (not (lessp x y))))
  296.          (equal (power-eval (power-rep i base)
  297.                 base)
  298.             (fix i))
  299.          (equal (power-eval (big-plus (power-rep i base)
  300.                       (power-rep j base)
  301.                       (zero)
  302.                       base)
  303.                 base)
  304.             (plus i j))
  305.          (equal (gcd x y)
  306.             (gcd y x))
  307.          (equal (nth (append a b)
  308.              i)
  309.             (append (nth a i)
  310.                 (nth b (difference i (length a)))))
  311.          (equal (difference (plus x y)
  312.                 x)
  313.             (fix y))
  314.          (equal (difference (plus y x)
  315.                 x)
  316.             (fix y))
  317.          (equal (difference (plus x y)
  318.                 (plus x z))
  319.             (difference y z))
  320.          (equal (times x (difference c w))
  321.             (difference (times c x)
  322.                 (times w x)))
  323.          (equal (remainder (times x z)
  324.                    z)
  325.             (zero))
  326.          (equal (difference (plus b (plus a c))
  327.                 a)
  328.             (plus b c))
  329.          (equal (difference (add1 (plus y z))
  330.                 z)
  331.             (add1 y))
  332.          (equal (lessp (plus x y)
  333.                (plus x z))
  334.             (lessp y z))
  335.          (equal (lessp (times x z)
  336.                (times y z))
  337.             (and (not (zerop z))
  338.              (lessp x y)))
  339.          (equal (lessp y (plus x y))
  340.             (not (zerop x)))
  341.          (equal (gcd (times x z)
  342.              (times y z))
  343.             (times z (gcd x y)))
  344.          (equal (value (normalize x)
  345.                a)
  346.             (value x a))
  347.          (equal (equal (flatten x)
  348.                (cons y (nil)))
  349.             (and (nlistp x)
  350.              (equal x y)))
  351.          (equal (listp (gopher x))
  352.             (listp x))
  353.          (equal (samefringe x y)
  354.             (equal (flatten x)
  355.                (flatten y)))
  356.          (equal (equal (greatest-factor x y)
  357.                (zero))
  358.             (and (or (zerop y)
  359.                  (equal y 1))
  360.              (equal x (zero))))
  361.          (equal (equal (greatest-factor x y)
  362.                1)
  363.             (equal x 1))
  364.          (equal (numberp (greatest-factor x y))
  365.             (not (and (or (zerop y)
  366.                   (equal y 1))
  367.                   (not (numberp x)))))
  368.          (equal (times-list (append x y))
  369.             (times (times-list x)
  370.                (times-list y)))
  371.          (equal (prime-list (append x y))
  372.             (and (prime-list x)
  373.              (prime-list y)))
  374.          (equal (equal z (times w z))
  375.             (and (numberp z)
  376.              (or (equal z (zero))
  377.                  (equal w 1))))
  378.          (equal (greatereqpr x y)
  379.             (not (lessp x y)))
  380.          (equal (equal x (times x y))
  381.             (or (equal x (zero))
  382.             (and (numberp x)
  383.                  (equal y 1))))
  384.          (equal (remainder (times y x)
  385.                    y)
  386.             (zero))
  387.          (equal (equal (times a b)
  388.                1)
  389.             (and (not (equal a (zero)))
  390.              (not (equal b (zero)))
  391.              (numberp a)
  392.              (numberp b)
  393.              (equal (- a 1)
  394.                 (zero))
  395.              (equal (- b 1)
  396.                 (zero))))
  397.          (equal (lessp (length (delete x l))
  398.                (length l))
  399.             (member x l))
  400.          (equal (sort2 (delete x l))
  401.             (delete x (sort2 l)))
  402.          (equal (dsort x)
  403.             (sort2 x))
  404.          (equal (length (cons x1
  405.                   (cons x2
  406.                     (cons x3 (cons x4
  407.                                (cons x5
  408.                                  (cons x6 x7)))))))
  409.             (plus 6 (length x7)))
  410.          (equal (difference (add1 (add1 x))
  411.                 2)
  412.             (fix x))
  413.          (equal (quotient (plus x (plus x y))
  414.                   2)
  415.             (plus x (quotient y 2)))
  416.          (equal (sigma (zero)
  417.                i)
  418.             (quotient (times i (add1 i))
  419.                   2))
  420.          (equal (plus x (add1 y))
  421.             (if (numberp y)
  422.             (add1 (plus x y))
  423.               (add1 x)))
  424.          (equal (equal (difference x y)
  425.                (difference z y))
  426.             (if (lessp x y)
  427.             (not (lessp y z))
  428.               (if (lessp z y)
  429.               (not (lessp y x))
  430.             (equal (fix x)
  431.                    (fix z)))))
  432.          (equal (meaning (plus-tree (delete x y))
  433.                  a)
  434.             (if (member x y)
  435.             (difference (meaning (plus-tree y)
  436.                          a)
  437.                     (meaning x a))
  438.               (meaning (plus-tree y)
  439.                    a)))
  440.          (equal (times x (add1 y))
  441.             (if (numberp y)
  442.             (plus x (times x y))
  443.               (fix x)))
  444.          (equal (nth (nil)
  445.              i)
  446.             (if (zerop i)
  447.             (nil)
  448.               (zero)))
  449.          (equal (last (append a b))
  450.             (if (listp b)
  451.             (last b)
  452.               (if (listp a)
  453.               (cons (car (last a))
  454.                 b)
  455.             b)))
  456.          (equal (equal (lessp x y)
  457.                z)
  458.             (if (lessp x y)
  459.             (equal t z)
  460.               (equal f z)))
  461.          (equal (assignment x (append a b))
  462.             (if (assignedp x a)
  463.             (assignment x a)
  464.               (assignment x b)))
  465.          (equal (car (gopher x))
  466.             (if (listp x)
  467.             (car (flatten x))
  468.               (zero)))
  469.          (equal (flatten (cdr (gopher x)))
  470.             (if (listp x)
  471.             (cdr (flatten x))
  472.               (cons (zero)
  473.                 (nil))))
  474.          (equal (quotient (times y x)
  475.                   y)
  476.             (if (zerop y)
  477.             (zero)
  478.               (fix x)))
  479.          (equal (get j (set i val mem))
  480.             (if (eqp j i)
  481.             val
  482.               (get j mem)))))))
  483.  
  484.   (defun tautologyp (x true-lst false-lst)
  485.     (cond ((truep x true-lst)
  486.        t)
  487.       ((falsep x false-lst)
  488.        nil)
  489.       ((atom x)
  490.        nil)
  491.       ((eq (car x)
  492.            (quote if))
  493.        (cond ((truep (car (cdr x))
  494.              true-lst)
  495.           (tautologyp (car (cdr (cdr x)))
  496.                   true-lst false-lst))
  497.          ((falsep (car (cdr x))
  498.               false-lst)
  499.           (tautologyp (car (cdr (cdr (cdr x))))
  500.                   true-lst false-lst))
  501.          (t (and (tautologyp (car (cdr (cdr x)))
  502.                      (cons (car (cdr x))
  503.                        true-lst)
  504.                      false-lst)
  505.              (tautologyp (car (cdr (cdr (cdr x))))
  506.                      true-lst
  507.                      (cons (car (cdr x))
  508.                        false-lst))))))
  509.       (t nil)))
  510.  
  511.   (defun tautp (x)
  512.     (tautologyp (rewrite x)
  513.         nil nil))
  514.  
  515.   (defun boyer-test ()
  516.     (let ((term
  517.        (apply-subst
  518.         (quote ((x f (plus (plus a b)
  519.                    (plus c (zero))))
  520.             (y f (times (times a b)
  521.                 (plus c d)))
  522.             (z f (reverse (append (append a b)
  523.                       (nil))))
  524.             (u equal (plus a b)
  525.                (difference x y))
  526.             (w lessp (remainder a b)
  527.                (member a (length b)))))
  528.         (quote (implies (and (implies x y)
  529.                  (and (implies y z)
  530.                       (and (implies z u)
  531.                        (implies u w))))
  532.                 (implies x w))))))
  533.       (tautp term)))
  534.  
  535. (deflocal ans ())
  536.  
  537. (defun boyer-short-test ()
  538.   (let ((term
  539.      (apply-subst
  540.       (quote ((x f (plus (plus a b)
  541.                  (plus c (zero))))
  542.           (y f (times (times a b)
  543.                   (plus c d)))
  544.           (z f (reverse (append (append a b)
  545.                     (nil))))
  546.           (u equal (plus a b)
  547.              (difference x y))
  548.           (w lessp (remainder a b)
  549.              (member a (length b)))))
  550.       (quote (implies (and (implies x y)
  551.                    (and (implies z u)
  552.                     (implies u w)))
  553.               (implies x w))))))
  554.     (setq ans (tautp term))))
  555.  
  556. (defun boyer-very-short-test ()
  557.   (let ((term
  558.      (apply-subst
  559.       (quote ((x f (plus (plus a b)
  560.                  (plus c (zero))))
  561.           (y f (times (times a b)
  562.                   (plus c d)))
  563.           (z f (reverse (append (append a b)
  564.                     (nil))))
  565.           (u equal (plus a b)
  566.              (difference x y))
  567.           (w lessp (remainder a b)
  568.              (member a (length b)))))
  569.       (quote (implies x y)))))
  570.     (print term)
  571.     (setq ans (tautp term))))
  572.  
  573.   (defun trans-of-implies (n)
  574.     (list (quote implies)
  575.       (trans-of-implies1 n)
  576.       (list (quote implies)
  577.         0 n)))
  578.  
  579.   (defun trans-of-implies1 (n)
  580.     (cond ((= n 1)
  581.        (list (quote implies)        
  582.          0 1))
  583.       (t (list (quote and)
  584.            (list (quote implies)
  585.              (- n 1)
  586.              n)
  587.            (trans-of-implies1 (- n 1))))))
  588.  
  589.  
  590.   (defun truep (x lst)
  591.     (or (equal x (quote (t)))
  592.     (member x lst equal)))
  593.  
  594. (boyer-setup)
  595. ;;(defvar setup-performed-p t)
  596.  
  597.   (defun testboyer ()
  598.     (let ((xx (cpu-time)))
  599.       (print (boyer-test))
  600.       (- (cpu-time) xx)))
  601.  
  602.   (defun testshortboyer ()
  603.     (print (boyer-short-test)))
  604.  
  605.   (defun testveryshortboyer ()
  606.     (print (boyer-very-short-test)))
  607.  
  608. )                    ; end of module
  609.